REF, NoConds
\\[0ex]Subst' $x$ \$b $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Subst' $x$ ( \$b)$\cdot$